T:Type, eq:EqDecider(T), es:ES, x, i:Id.
@i(x:T)  e@i. e'[lastchange(x;e),e).(x after e') = (x when e)  T 

latex

Definitions	ff, tt, if b then t else f fi , x. t(x), Top, P  Q, P & Q, P  Q, , t  T, lastchange(x;e), e@i. P(e), @i(x:T), P  Q, EqDecider(T), x:A. B(x), Unit, , x(s),
Lemmas	assert of bnot, eqff to assert, iff transitivity, eqtt to assert, alle-between1-trivial, not wf, bnot wf, last-change-after-property, es-vartype wf, es-isconst wf, changed wf, assert wf, iff wf, bool wf, event system wf, es-dtype wf, es-E wf, es-loc wf, Id wf